1. Field of the Invention
The present invention relates to verification of a design description using a property description language.
2. Description of the Related Art
Design of a system mainly including electronic circuits extensively uses a method that describes properties (constraints on the design of an object) by using a property description language based on the temporal logic or regular expression, and verifies a design description on the basis of the property description.
The property description generally constrains part of design, and does not constrain the whole design description in most cases. Also, it is generally impossible to cover all the behaviors of a system designed by using the property description.
On the other hand, when examining the design description with the property description, the behavior of a portion given the property description can be examined, but that of a portion given no property description cannot be examined. That is, the design description examined using the property description is divided into three portions: (1) a portion having passed the examination, (2) a portion having failed the examination, and (3) an unexamined portion (inactive description). Mixing of particularly the third inactive description is unavoidable due to the above-mentioned characteristics of the property description. Since, however, this inactive description cannot be distinguished from the portion having passed the examination, the existence of the inactive description is an essential problem in an examination using the property description.
“Have I written enough properties?”—A method of comparison between specification and implementation, Sagi Katz, Orna Grumberg, In poc. of CHARME '99, 1999 discloses a method which uses simulation relation, but takes coverage on the automaton of the property.
U.S. Pat. No. 6,484,134, Yatin V. Hoskote, “PROPERTY COVERAGE IN FORMAL VERIFICATION” discloses a system which computes the coverage in which a change in an observable proposition will not affect the correctness of the property. The system does not use simulation relation in it.